// Scalina

grammar
  l, L, x metavars (value labels, type labels, variables)
   // instantiation | selection | refinement
  t = x
    | t "." l   
    | t "<{" cm "}"   
    | "new" T       
  p = ... // subset of terms -- until we add effects, could include all terms
  v = "new" T
  
  T = T "#" L 
    | T "<{" cm "}"  
      // would correspond to object literal term, but we use `new T` for that
    | "{" bind(x) (":" T)? "=>" in(m*) "}" = R 
    | T "&" T   // if we had split objects, would correspond to merging them
    | p "." type  // useful for type-level computation
    | "Any" | "Nothing" // for the subtyping lattice
    // Any is used to subsume types dependent on the root
    // object, as the main expression cannot select one of its members 
    // that is typed as another member because then the root's self variable
    // would escape its scope
    | "Un[" T "]" // the type of a deferred value member,
    // TODO: or of any type that contains members with this type
    
  m = 
// abstract or deferred value member
// an abstract member must be overridden by a concrete member before 
// the class can be instantiated 
      "val" l ":" T

// a concrete value member
    | "val" l ":" T "=" t
       
// abstract or deferred type member
    | "type" L ":" K
    
// concrete type members are statically bound 
// --> kind is in invariant position
// type L : In(T & U, T & U)  can be made concrete with T & U or U & T, 
// so abstract type members with kind In(T, T) do not subsume concrete type
// members or singleton kinds (not present in Scalina ATM)
    | "type" L ":" K "=" T    
    
/*
[to declare an abstract value member, you specify its label and the type that 
classifies valid concretisations of that member]
--> to declare an abstract type member, you specify its label and the kind 
that classifies valid concretisations of that member

[when you select a member on an object, you derive the type of the object and 
check the definition of that member in the type]
--> when you select a member on a type, you derive the kind of the type and 
check the definition of that member in the kind

entanglement of subtyping and subkinding is worrying

TODO: can we use exact types by default and track when subsumption was used by 
giving types a different kind? 
*/
  K = 
// the kind of type members that must be refined before a member of the 
// enclosing type may be selected -- behaves contravariantly
      "Un[" K "]" 

// the kind of bounded abstract type members -- 
// if the bounds contain no un-members, type members may be selected on 
// types of this kind (different from nuObj)
    | "In(" T "," T ")"  

/* 
like a type tracks the members that are available on the values it classifies, 
 a kind tracks the (value&type) members available on the types it classifies 

Types that have R as a structural supertype are classified by Struct(R) 
 -- note that kind subsumption may make this a very rough approximation 
    of the actual type, although un-members are never forgotten  
     
 `*` is syntactic sugar for `Struct({x =>})`
*/
    | "Struct(" R ")"
  
/*
The kind that classifies a nominal type, similar to Struct(R), except that
bindings classified by Nominal(_) are not traversed during normalisation
*/
    | "Nominal(" R ")"

/** Concrete(R) classifies types...
  - that may be instantiated (structural type, nominal type), 
      but also singleton types, which may not be instantiated;
  - on which the type members in R may be selected 
    (singleton, type with only concrete type members)
*/
    | "Concrete(" R ")"
    
    
/* no type annotation because can't
refer to self variable, which would often be needed if type must be specified 
underlying simplification: refinement does not have recursion through self */
  cm = "val" l "=" t | "type" L "=" T  
  
  G = empty | x ":" T, G
  
rules
  adding_to_set_members =
    mems1 -+ mems2 = members from mems1 not in mems2 + members in mems2
    mems -+ mem = mems w/o member with same label as mem + mem
    
// relate canonical type to its structural representation 
// (it has been fully reduced by the type "evaluation" rules)
// T <:~ T' and G |- T' <: U implies T <: U
// T <:~ T' if T' is the least structural type so that G |- T <: T'
// traverses Nominal type bindings (they are related to the structural type
// containing their members)
// notes:
//  - T cannot depend on a path

// TODO: check that this relation considers every type encountered during eval  
  to_structural = T "<:~" T
      R <:~ R // only need reflexivity, transitivity is distributed over rules
   
      { x : S => mems } <:~ { x : S => mems }
      { x => mems } <:~  { x : { x => mems } => mems }
            
      T1 & T2 <:~ { x : S1 & S2 => mems1 -+ mems2 } // m2 overrides m1
        if  T1 <:~ { x : S1 => mems1 }
            T2 <:~ { x : S2 => mems2 }

      T # L <:~ R
        if  T <:~ {x => mems}
            mems contains `type L : _ = S`
            x \notin FV(S)
            S <:~ R
            
      (new T).type <:~ R // only path we encounter at run time (?)
        if  T <:~ R


//TODO:
  lookupT = T "has" m "under" x ":" T
  
    T has m under x : S
      if  T <:~ {x : S => mems}
          mems contains m

  
  eval = 
    // LHS is a path, must evaluate to a path 
    // (only select value members with RHS = path)
    // we want to model looping programs with looping evaluations 
    // `(new {x => val a = x.a}).a` should not get stuck
    // general case: need context rule to reduce RHS to a path
    // must use new T instead of new { ... } since if we only eval on 
    // new of structural type, need context rule that turns Nominal type
    // into structural one, but that's not type preserving  
    (new T).l  ==>  [x -> new T]p  // eval/sel
      if  T has `val l: U = p` under x : _
      
    // refine-with-path (cf. call-by-path)
    // note the type we give to l (`p.type`), due to a technicality in the
    // proof of preservation, can't use U from the lookup (p.type is more
    // precise anyway)
    // eval/refine/v
    
    // [Frank] checking type information in operational semantics!
    // 
    (new T) <{val l = p}  ==>  new ( T <{val l = p} )
      if  T has `val l: Un[_]` under _ : _

    // eval/refine/t
    (new T) <{type L = U}  ==>  new ( T <{type L = U} )
      if  T has `type L : Un[_]` under _ : _


    // "silent transition" to evaluate RHS of value members to paths, so that
    // they may be selected by rule eval/sel
    // TODO: experiment! is this enough for progress? how does it interact
    //       with deferred members?
    // TODO!!! what it there's no 1-step reduction from the RHS to a path?
    new T ==> new (T & {_ => val l: p.type = p}) // eval/ctx/new
      if  T has `val l: U = t` under x : S
          [x -> new T]t ==> p // replace x since we don't have a store to
                              // track it

// TODO!!! what it there's no 1-step reduction from t to a PATH p?
// must reduce to path for type preservation 
    C[t] ==> C[p] // eval/ctx/v
      if  t ==> p

    // C relates a term t to terms that embed this t
    C[t] = t | t1 <{val l = C[t]} | C[t] <{val l = p} | C[t].l 



  // typing judgement
  of = G "|-" t ":" T 


/*** of/new
T may have un-members but type of self variable (S) considers them normal 
members a member on the object can only be accessed when there are no 
un-members in its type, and self variable can only be accessed as a result
of a member on the object being accessed, so the self variable can never be 
used when it refers to an incomplete object (one with un-members)

the actual type of the self variable (as opposed to the expected type S)
is the type that's instantiated (T)

instantiation is an operation on a type, thus it is determined by kinding

TODO: must T be a type value?
*/
    G |- new T : T
      if  
          // expand type to exact list of members, then use kinding to check
          // they're WF and non-abstract
          G |- T ~~< {x: S => mems}
          // also used in kinding type selection, where subsumption is ok
          G |- {x: S => mems} : Concrete({x: S => mems})  // leave like this
          T is not a singleton type // Singleton types are also considered
           // concrete, as they're a safe target for type member selection.
           // However, they cannot be instantiated.

/*** of/selpath
 must not be any deferred members left, 
 abstract is allowed when accessing members on the self variable 
 (ruled out when instantiating)
*/
    G |- p.l : [x -> p]U 
// --> check for `val l : U` or `val l : U = t` --> subsumption cannot forget
// deferred members, thus this is safe (concrete member is subsumed to 
// abstract member, but deferred member stays deferred & cannot be omitted)
      if  G |- p : {x => val l : U} // use subsumption to forget other members 

// of/sel -- t is not a path (due to ordering of rules)
    G |- t.l : U/*'*/ 
      if  G |- t : {x => val l : U} 
      //  G |- U ~~> U' // TODO: allow type selections that do not involve x
          x \notin FV(U/*'*/) // self variable x must not escape its scope
                        // (can't replace it by t since t is not a path)

/*** of/refine/v
 refining deferred value member l of term t with concrete value u

- for soundness, type of value must be in contravariant position (Un[T])
- this is not imperative assignment, but delayed initialisation, 
  so only allow to "write" to abstract value once 
    --> subsumption cannot forget un-members
- once value is initialised, its type is in a covariant position, 
  otherwise it could not be read 
- need both mixins and refinement --> refinement changes the type of the 
  refined member from Un[T] to T -- mixin composition isn't allowed to do that
*/
    G |- t <{ val l = u }   :  T <{val l = u}
      if  G |- t : T
          T has `val l : Un[U]` under x : S 
          // or just G |- t : {x: S => val l : Un[U]} 
            // --> NO! subsumption does not forget un-members
          G, x: S |- u : U
          x \notin FV(u)

// of/refine/t: refining deferred type member L of term t with concrete type U
    G |- t <{ type L = U }   :  T <{type L = U}
      if  G |- t : T
          T has `type L : Un[K]` under x : S // (1), (2)
          G, x: S |- U : K
          x \notin FV(U)

// of/single 
// this rule gives a path its most precise type (the inverse of subsumption,
// which weakens the type)
    G |- p : p.type
      if  G |- p : T
          T is not a singleton type  // TODO: require T to be a structural type?

// of/subsume
    G |- t : S      
      if  G |- t : T
          G |- T <: S


// TODO
  pathConversion = G "|-" p ~~> p
    G |- p1.l ~~> [x -> p1]p2
      if  G |- p1 : {x => val l : _ = p2}

// reflexive, transitive and symmetric closure of p ~~> p
  pathEquality = G "|-" p =~= p
// TODO

// DOES NOT DO SUBSUMPTION --> the list of members retrieved this way must
// contain ALL THE MEMBERS in the type
// canonical form for types: 
//    (T1 <{...} ... <{...}) & ... & (Tn <{...} ... <{...}) & {...}
// with (Ti <{...} ... <{...}) : Nominal(_)
  typeConversion = G "|-" T ~~> T
// TODO
  // - perform type member selections except for Nominal bindings
  //    --> Nominal bindings must be opaque (for subtyping)
  // - perform value member selections ???
  //    --> this could solve the problem with type preservation for the
  //        context rule in the target of value member selection 
  //        (t.l.type <: p.type if t has `val l: _ = p`)

// analogy with opsem for value member selection: don't check kinds
    G |- {x => type L : _ = S}#L ~~> S
    
    G |- {x : S1 => mems1} & {x : S2 => mems2} ~~> {x : S2 => (mems1 -+ mems2}
      if  G |- S2 <: S1
          mems2 forall{m2 => (mems1 has m2.label) implies 
                                  G |- m2 <: mems1(m2.label) }
// TODO 
// TODO: what with T1 & T2 if Ti : In(S, T)    
    
// TODO: context rule to rewrite T#L to T'#L if T ?? T' ?s

    G |- T#L ~~> S#L
      if  G |- T ~~> S

    G |- T <{_} ~~> S <{_}
      if  G |- T ~~> S

    G |- T1 & T2  ~~> S1 & S2
      if  G |- T1 ~~> S1
          G |- T2 ~~> S2

    G |- p.type ~~> q.type
      if G |- p =~= q
      
    G |- Un[T] ~~> Un[S]
      if  G |- T ~~> S
            
      
// Note that only concrete type members with a kind of the shape Nominal(_)
// are not traversed (nominal type bindings are opaque)
    G |- p.type#L ~~> [x -> p]S 
      if  G |- p.type <: {x : _ => type L : K = S}  // TODO: okay to use <: ?
          K not of shape Nominal(_)

    G |- T#L ~~> S 
      if  G |- T <: {x : _ => type L : K = S} // TODO: okay to use <: ?
          K not of shape Nominal(_)
          x \notin FV(K, S)  
          
/* TODO:
T : Struct({self => 
  type T1: * = self.type#T2
  type T2: * = Any })
  
T#T1 ~~> Any ?
*/

// TODO: what does x.type#T & { type L = U }  normalise to?

// reflexive, transitive and symmetric closure of T ~~> T
  typeEquality = G "|-" T =~= T
// TODO


// TODO
// type conversion + traverse nominal type bindings
// DOES NOT DO SUBSUMPTION 
  typeExpansion = G "|-" T ~~< T
    G |- T ~~< S
      if  G |- T ~~> S

    G |- p.type#L ~~< [x -> p]S 
      if  G |- p.type <: {x : _ => type L : Nominal(_) = S} 

    G |- T#L ~~< S 
      if  G |- T <: {x : _ => type L : Nominal(R) = S}
          x \notin FV(R, S)  

// include widening in expansion
    G |- p.type ~~< T
      if  G |- p : T

// TODO: do normal subtyping check, but ignore Un[_] in classifiers
  subtypingIgnoringDeferred = G "|-" T "<[]:" T
  
  
  subtyping = G "|-" T "<:" T
    
      G |- T <: T
      G |- S <: U
        if  G |- S <: T
            G |- T <: U

      G |- T <: Any
        if  G |- T : K // TODO: necessary?
        
      G |- Nothing <: T 
        if  G |- T : K // TODO: necessary?
      
      G |- Un[S] <: Un[T] // deferred value members behave contravariantly
        if  G |- T <: S

// include type conversion into subtyping
// a nominal type is NOT =~= the structural type it expands to
      G |- S <: T
        if  G |- S =~= T

// TODO: members with un-types must not be forgotten
// member with a normal type is a promise to the client
// member with an un-type is a requirement of the client (i.e., the client has
// to refine it before it can select any member on the object)
// subsumption is about weakening a type's /promise/ to a client, but omitting 
// members with un-types weakes the /requirement/ of the client
      G |- {x : S => mems} <: {x : S2 => mems2}
        if  G |- S <: S2
            forall m1 in mems, 
              (mems2 has m2 with same label as m1 && 
               G, x : S |- m1 <: m2) || not (m1 deferred).


// ??   G |- x.type#L <: S#L   if G |- x : S and L is not deferred
      
// TODO: never forget un-members! 
// TODO: what about abstract type members.. cf. kinding of S & T
      G |- T1 & T2 <: T1
      G |- T1 & T2 <: T2
      G |- T <: T1 & T2
        if G |- T <: T1
           G |- T <: T2

// TODO: do we want/need this
      G |- T <: S
        if  G |- T : In(_, S) // due to kind subsumption, don't need to check for other kinds (they are all subsumed to this one)


      G |- p.type <: T // sub/single
        if  G |- p : T // handles path expansion:
          // if  G |- p : q.type --> p.type <: q.type --> path equality

                
  memsub = G "|-" m "<:" m
/***
 reflexivity and transitivity are derivable (TODO: check this)

 a value member is a submember of another value member if their declared types 
 are subtypes (covariantly, the rule for subtyping un-types reverse subtyping 
   so that they behave contravariantly)
 
 a type member is a submember of another type member if their declared kinds 
 are subkinds 
  ADDITIONALLY, unlike value members, a concrete type member does not have 
  submembers (except itself) 

 the following rules are NOT ADMISSIBLE:
   - member <: deferred member
 --> would allow subsuming an already initialised member to a 
     deferred one and "re-initialise"!
*/
      
// important: actual value RHS does not matter, only declared types
//  -- correspondence is enforced by well-formedness      
      G |- val l : T (= _)? <: val l : T' (= _)? // memsub/v
        if G |- T <: T'
      
      G |- type L : K (= _)?  <:  type L : K'
        if  G |- K <: K'

// (this is one of the rules that has to be dropped to support virtual classes)
      G |- type L : K = _   <:  type L : K = _ 


  WFmem = G "|-" m "WF"
      G |- val l : T = t WF // WF/v/concrete
        if  G |- t : T

      G |- type L : Nominal(R) = T  WF // WF/t/nominal
        if  G |- T : Struct(R) // dealing with Nominal types is a mess!!!
          
      G |- type L : K = T  WF // WF/t/concrete
        if  G |- T : K

// if we don't check well-formedness of declared classifiers, 
// --> subtyping/-kinding is checked for possibly ill-formed types/kinds when
// deciding submembering
      G |- val l : T  WF  // WF/v/non-concrete  (abstract or deferred)
      G |- type L : K WF  // WF/t/non-concrete  (abstract or deferred)



  kinding = G "|-" T ":" K

// counterpart of typing `new T` (but distinguish types that may contain
// abstract members from those that must not)

// 1) some mems may be abstract
    G |- {x: S => mems} : Struct({ x : S => mems }) 
      if  mems forall {m => G, x : S |- m WF }
// needed in preservation case 1 (to be able to appeal to substitution lemma)
// problematic: T may contain deferred members, but S may list these as
// non-deferred need special type constructor StripDeferred[T], which modifies
// subtyping so that when members are expanded, the deferred modifiers are
// stripped in the corresponding case of the preservation proof, there are no
// deferred members left, as it was ok to select a member on a term of type T
          G |- T <[]: S
          mems no_duplicates
          
    G |- T1 & T2 : Struct({x : S2 => (mems1 -+ mems2})
      if  G |- T1 : Struct({x : S1 => mems1})
          G |- T2 : Struct({x : S2 => mems2})
          G |- S2 <: S1
          mems2 forall{m2 => (mems1 has m2.label) implies 
                                  G |- m2 <: mems1(m2.label) }

// 2) all mems are known to be concrete
// check that the given subset of the members of T are WF and non-abstract
    G |- T : Concrete({x: S => mems})
// type normalisation that also crosse nominal type bindings
      if  G |- T : Struct({x: S => mems}) // check WF'ness of members
// no abstract members (un-members allowed of course)
          mems forall {m => m deferred XOR m concrete } 

    G |- p.type : Concrete({x: S => mems}) 
      if  G |- p : T
          G |- T : Struct({x: S => mems})

// counterpart of typing value member selection
// if T in T#L is (or abstracts over) a type which necessarily only has
// concrete members, 
// or if we simply know the concrete RHS of L in T (Concrete is used to check
// a subset of the members)
// of/k/selsingle
    G |- p.type#L : [x -> p]K 
      if  G |- T : Concrete({x => type L : K})

// of/k/sel
    G |- T#L : K 
      if  G |- T : Concrete({x => type L : K})
          x \notin FV(K)

// there's never a need to *infer* the kind Nominal(_), it's only specified
// explicitly by the programmer (introduced into kind checking via type member
// selection)
  
// counterpart of typing member refinement
    // of/k/refine/v 
    G |- T <{ val l = u } : Struct({x : S => mems -+ `val l : U = u`}) 
      if  G |- T : Struct({x: S => mems}) 
// the `x` above is fresh, because `contains` looks under the binder
          mems contains `val l : Un[U]`
          G, x: S |- u : U
//          x \notin FV(u) // automatically the case, as x is fresh

    // of/k/refine/t
    G |- T <{ type L = U } : Struct({x : S => mems -+ `type L : K = U`}) 
      if  G |- T : Struct({x: S => mems}) // x fresh
          mems contains `type L : Un[K]`
          G, x: S |- U : K
//          x \notin FV(U)

// subsumption
    G |- T : K2 // of/k/subsume
      if  G |- T : K1
          G |- K1 <: K2

// rules without typing-counterparts:
    G |- Any : Struct({x =>})
    G |- Nothing : Struct({x =>})

// an un-type is simply well-kinded if the type it turns into after refinement 
// is well-kinded
// TODO: think about this more
    G |- Un[T] : K
      if  G |- T : K
      

  subkinding = G "|-" K "<:" K

    G |- Un[K1] <: Un[K2] // deferred type members behave contravariantly
      if  G |- K2 <: K1

    G |- Nominal(R) <: Struct(R)
    G |- Concrete(R) <: Struct(R)

// if a type T >: T1 <: T2 was expected, may pass any type S with
// LEAST structural supertype R
// NOTE: cannot replace Struct by * (lower bound would not be satisfied)
    G |- Struct(R) <: In(S, T) 
      if  G |- S <: R
          G |- R <: T
    
// if we know a type has concrete versions of all members in R1, it will also
// have concrete ones for R2 >: R1
    G |- Concrete(R1) <: Concrete(R2) 
      if  G |- R1 <: R2 

    G |- Struct(R1) <: Struct(R2) 
      if  G |- R1 <: R2 

// a bounded abstract type member may be overridden with an abstract type 
// member with stricter bounds (covariance)
// TODO: checks kinds (as well as / instead of) types (see paper)
    G |- In(T1, T2) <: In(S1, S2) 
      if  G |- T2 <: S2
          G |- S1 <: T1

// TODO
// if U : Struct(R)  is expected, U' : In(S, T) will do if T : Struct(R)
// if T does not have deferred members, neither will U
//    G |- In(S, T) <: Struct(R)
//      if  G |-  T : Struct(R)

      
/* TODO: this does not make sense, I think:
    G |- In(T1, T2) <: Struct(R)
      if  G |-  T1 : Struct(R)
*/

  kind and context formation = G "|-" K
  // TODO

      
                       
  cnc = m "concrete" // trivial
  abs = m "abstract" // trivial
  dfr = m "deferred" // trivial